1. Field of the Invention
The present invention relates to the field of hardware circuit verification, specifically to verifying identical functionality between two different logic level circuit models. In particular, it relates to a logic verification method that uses a distributed computing environment to quickly solve difficult verification problems.
2. Background of the Related Art
Recent increases in the complexity of modem integrated circuits have resulted in corresponding increases in the difficulty of verifying design correctness. Design flaws have significant economic impact both in terms of increased time-to-market and in reduced profit margins. A typical design flow has many steps, each of which can introduce design flaws. Traditionally, simulation-based techniques have been used to verify design correctness. These techniques have become less effective because of their inability to completely and quickly verify large designs. An increasing popular alternative is the use of formal mathematical techniques, employed by tools known as equivalence checkers, to verify design correctness.
A typical design flow where an integrated circuit is taken from concept to fabrication includes a number of steps. As a first step, the conceptual nature of the integrated circuit is determined. The desired functionality of a circuit is described by a set of specifications. A conceptual model of the circuit is created based on the specifications. For example, in the case of a complex microprocessor, the conceptual nature of the circuit is typically specified in a high level language such as C++. Modeling tools are available which simulate the behavior of the conceptual model under specific test cases to ensure that the model performs as expected.
Once the conceptual nature of the circuit is determined, a register transfer level (RTL) model of the digital circuit is built based upon the conceptual model and is modeled on a digital computer using an RTL modeling tool. At this stage, the design of the circuit, as modeled by the RTL modeling tool, may be used to verify that the circuit meets the desired specifications. In some cases the RTL modeling tool may allow the validity of the modeled circuit to be checked in the context of the high-level language model.
After the design of the RTL model is completed, it is transformed into a gate level model in which individual logic gates are specified and connected together to perform the same logic functions as the RTL level circuit model. The transformation process is error-prone due to both human error and tool error. To validate the transformation, the logic functions of the gate level model must be verified to be the same as the corresponding functions in the RTL model. An equivalence checking tool, such as one described in this invention, can be used to perform this verification.
The gate level model is often further transformed by optimizations that attempt to improve the performance of the circuit such as reducing the area required to construct the circuit, increasing the speed of operation of the circuit and reducing the power consumption of the circuit. Once the gate level logic of the circuit model has been optimized, the optimized gate level model operation must be verified with respect to either the RTL level model or the original gate level model.
The gate level model may go though additional transformations, each yielding successive versions of the circuit. An example of this transformation is scan logic insertion, which allows the circuit to perform in a scan mode and a normal mode. When operating in scan mode the circuit can be tested for manufacturing defects, while in normal mode the circuit should behave as before. Another example is clock tree insertion, which is the process of inserting buffers in the clock tree to improve the timing of clock signals.
At some stage the gate level circuit is placed and routed into a layout. This step may involve further transformations and local optimizations that are driven by placement and timing constraints. Each transformation necessitates the verification of functionality of the pretransformation version compared with the post-transformation version of the circuit.
Conventional equivalence checking tools can be used to verify the functional equivalence of each pre-transformation version versus the corresponding post-transformation version. The verification can be performed by comparing the post-transformation version with either the first RTL circuit model or with a previously verified pre-transformation version. Significant resources (engineering time, computer time and computer memory) are used to perform this verification. Conventional equivalence checking tools frequently fail to complete because of these resource limitations.
In conventional circuit verification, equivalence checking of two circuits is performed by (1) partitioning the two circuits into corresponding combinational subcircuit pairs that contain no storage elements, and (2) sequentially verifying the equivalence of each corresponding subcircuit pair. The circuits are partitioned at circuit inputs, outputs and storage element boundaries. The combinational subcircuit pairs are associated according to a correspondence between the circuit inputs, outputs and storage elements of the two circuits, so that the equivalence is verified for each corresponding set of subcircuits. The conventional device can create the circuit input, output and storage element correspondence with user guidance or automaticallyxe2x80x94see, e.g., U.S. Pat. No. 5,638,381 to Cho et al., U.S. Pat. No. 5,949,691 to Kurosaka et al. and Foster, xe2x80x9cTechniques for Higher-Performance Boolean Equivalence Verificationxe2x80x9d, Hewlett-Packard Journal 30-38 (August 1998).
Checking identical functionality of combinational subcircuit pairs is an inherently difficult problem. The resources used to perform the check are typically related to the structural differences of the two circuit models. Conventional equivalence checking tools often encounter combinational subcircuit pair checks that cannot be resolved with the allotted time and memory resources.
An example of this difficulty occurs when a combinational subcircuit contains a multiplier. Circuits containing multipliers are well known to be difficult from an equivalence checking perspectivexe2x80x94see, e.g., Bryant, xe2x80x9cGraph-Based Algorithms for Boolean Function Manipulationxe2x80x9d, IEEE Transactions on Computers, Vol. C-35, No. 8, August 1986, pp. 677-691. A standard method of addressing this shortcoming is for the user to intervene and manually partition each combinational subcircuit into two subparts. One subpart of each circuit model contains the multiplier and the other subpart the remainder of the circuit model. The multipliers are typically compared using traditional simulation based methods, while the other subparts can be compared using the conventional equivalence checking tool. The user must take care to partition the combinational subcircuits correctly, and must perform two different equivalence checks to compare the corresponding subparts. The technique of resolving difficult pair checks by splitting the combinational subcircuits into corresponding subparts can be applied to pair checks that do not involve multipliers as well.
Another method of resolving difficult pair checks is to perform case analysis. An illustrative example of a case analysis follows. First, an input to the difficult combinational subcircuit pair is chosen. Then two additional combinational subcircuit pairs are created; one in which the chosen input is assigned to the false value (0), and another in which the chosen input is assigned to the true value (1). Then each corresponding pair is compared using a conventional equivalence checking tool. The user must take care to assign the chosen inputs correctly and must perform two different equivalence checks.
Existing semiconductor design environments typically have significant distributed computing resources available. A design engineer often has convenient access to many workstations, or can access distributed computing resources through an application service provider (ASP), described in greater detail below. These additional resources could potentially be of significant use in addressing the verification problem. Conventional equivalence checking tools are unable to directly take advantage of these additional distributed resources. By manually partitioning the two circuit models into many subparts, the user can explicitly assign different subparts to each available distributed resource. The user must take care to partition the circuit models correctly, to execute each check correctly, and to correctly track and assemble the results of each of the subparts.
FIG. 1 illustrates a typical distributed computing environment, in which a collection of computing units such as workstations 110-113 can communicate and pass data to each other via a network 120-124. The network may range from a local area network to the Internet.
FIG. 2 shows the flow in a conventional system for doing equivalence checking as disclosed in the aforementioned Kurosaka et al. patent. The conventional system includes a data input section for reading descriptions of the two circuits to be compared. This system then detects corresponding inputs, outputs and storage elements in the two circuits. Following this, based on the corresponding storage elements in the two circuits, the circuits are partitioned into many smaller purely combinational portions. The system then has to check the functional equivalence of each pair of corresponding portion. Each check of functional equivalence between each pair of corresponding portions is hereinafter referred to as a pair check.
Each of the two circuits is represented in the system as a data structure composed of interconnections of elementary Boolean gates, such as AND gates, OR gates, NOT gates and the like, and storage elements such as latches and flip-flops. The elementary gates can be grouped together to form new components, which can be further used to create circuit models that are hierarchical in nature.
More specifically, having read the circuit data in the starting Step 200, the input pair, output pair and storage element pair correspondence between the two circuits is determined in Step 205. The storage elements may be flip-flops and latches, as well as tri-state elementsxe2x80x94see the aforementioned Cho et al. and Kurosaka et al. patents and the Foster paper for a detailed description of how to determine the correspondence. This reduces the problem of equivalence checking to the problem of checking the equivalence of pairs of combinational sub-circuits. Next an unchecked pair is selected in Step 210, and the pair is checked for equivalence in Step 215. The result of the pair check is saved in Step 220. When all unchecked pairs have been examined in Step 210, the system writes out the comparison results in Step 225.
To further aid in the understanding of the prior art and the problems associated therewith, it may be helpful to provide a brief overview of distributed computing environments. As used herein, a computing environment consists of an ensemble of processing units connected by a network. The network allows the processing units to communicate by passing data between themselves. The network may range from a local onboard bus to a local area network to a very large and expansive network such as a wide area network. The computing environment also includes the various operating systems, storage media, and other processing resources which reside on these computers and that are interconnected and accessible via the network through various software products.
The rapidly dropping cost of computer workstations and communication networks has significantly increased the amount of computing resources available in the typical engineering workplace environment: However, conventional equivalence checking tools are unable to take advantage of this commonly available additional resource. To use this additional resource, the user of the conventional equivalence checking tools must first manually partition the verification problem into a number of different problems. This partitioning may involve manual copying and editing of the versions of the design models being compared. In most cases, it is practically impossible for a user to create a fine-grained partition of the verification problem, which further restricts the user""s ability to use the distributed resource. Next the user must assign each partitioned problem to a different distributed computing resource. Finally, assuming that each partitioned problem was satisfactorily resolved, the user must manually combine all of the results together to determine the answer to the original verification problem. If any partitioned problem does not complete satisfactorily, the user must decide how to resolve the problem and complete the verification process. Each of these steps is time consuming, prone to human error and is an additional distraction to the user.
The Internet, coupled with the previously mentioned drop in computer and network resource costs, has resulted in the growth of ASPs. For a fee, an ASP provides access to a number of applications in an environment with a large available distributed computing resource. This enables businesses with limited financial resources to avail themselves of powerful distributed computing resources. To take advantage of the resources available from an ASP using a conventional equivalence checking tool, a user must manually perform the error prone process of partitioning, execution and recombination.
A much more desirable methodology would be to perform the process of check partitioning, distributed solution and subsequent recombination in an easy, automatic and less error-prone fashion. The present invention describes such an equivalence checking tool which automatically uses the available distributed computing resource.
The present invention relates to an equivalence checking system where checks on pairs of combinational subcircuits are performed concurrently in a distributed computing. environment. Each individual pair check is performed in a distributed computing environment by using the combinational equivalence checking portion of a known technology. Difficult pair checks can be solved by one of the following methods:
a cooperative divide-and-conquer approach which partitions a pair check into further, easier to solve, pair checks;
a competitive approach, in which a collection of equivalent pair checks replaces a difficult pair check; and
allocating additional resources to solve the pair check.
The present invention eliminates the error prone user intervention, and can automatically use additional resources available in a distributed computing environment.
A check manager can determine if the verification is complete by determining if all combinational subcircuit pairs have been checked. After all pair checks have been completed, the check manager can easily determine the overall status of the verification check by examining the finished check results. The check manager determines the overall verification status to be one of the following:
the designs are equivalent;
the designs are not equivalent; and
the allocated memory resources were exhausted before the designs could be proven to be equivalent or not equivalent.
If the third possibility occurs, the check manager may choose to run relevant portions of the task again with additional computing resources to attempt to complete the checking task with an equivalent or not equivalent result.
Prior verification methods combine the combinational pair check engine and all aspects of check management into a single-threaded program. In contrast, the current invention explicitly separates these elements, thus permitting verification problems to be solved in a scalable fashion. In addition, the current invention identifies additional techniques for addressing difficult pair checks that can dramatically improve performance and allow resolution of problems that had no practical solution before.